EKind{i:l}  Type{i'} 

latex

Definitions	P & Q, EventsWithKinds, EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), A, b, first(e), loc(e), Id, Top, t  T, pred(e), x:A. B(x), P  Q
Lemmas	pred wf, top wf, loc wf, first wf, assert wf, not wf, Id wf, EOrderAxioms wf, IdLnk wf, unit wf, deq wf